1  ((¬Q(0,0)∨(Q(0,M*0)∨¬∀I K.((¬(K=0)∧Q(I,K))⊃Q(PREDI,K+M))))∧∀N.((¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(K=0)∧Q(I,K))⊃Q(PR%
EDI,K+M))))⊃(¬Q(SUCCN,0)∨(Q(0,M*SUCCN)∨¬∀I K.((¬(K=0)∧Q(I,K))⊃Q(PREDI,K+M))))))⊃∀N.(¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(%
K=0)∧Q(I,K))⊃Q(PREDI,K+M))))    ∧I (INDUCTION) 

2  (M*0)=0    ∀E TIMES1 M 

3  ¬Q(0,0)∨Q(0,M*0)    TAUTEQ 

4  ¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(K=0)∧Q(I,K))⊃Q(PREDI,K+M)))  (4)  ASSUME 

5  ¬∀I K.((¬(K=0)∧Q(I,K))⊃Q(PREDI,K+M))⊃(¬Q(SUCCN,0)∨(Q(0,M*SUCCN)∨¬∀I K.((¬(K=0)∧Q(I,K))⊃Q(PREDI,K+M))))    TAU%
T 

6  ∀I K.((¬(K=0)∧Q(I,K))⊃Q(PREDI,K+M))  (6)  ASSUME 

7  ((SUCCN≥0⊃Q(SUCCN-0,M*0))∧∀N1.((SUCCN≥N1⊃Q(SUCCN-N1,M*N1))⊃(SUCCN≥SUCCN1⊃Q(SUCCN-SUCCN1,M*SUCCN1))))⊃∀N1.(SUC%
CN≥N1⊃Q(SUCCN-N1,M*N1))    ∧I (INDUCTION) 

8  Q(SUCCN,0)  (8)  ASSUME 

9  (SUCCN-0)=SUCCN    ∀E MINUS2 SUCCN 

10  SUCCN≥0⊃Q(SUCCN-0,M*0)  (8)  TAUTEQ 

11  SUCCN≥N1⊃Q(SUCCN-N1,M*N1)  (11)  ASSUME 

12  NATNUM(SUCCN-N1)⊃((¬((M*N1)=0)∧Q(SUCCN-N1,M*N1))⊃Q(PRED(SUCCN-N1),(M*N1)+M))  (6)  ∀E 6 SUCCN-N1 , M*N1 

13  SUCCN≥N1  (13)  ASSUME 

14  SUCCN≥N1⊃NATNUM(SUCCN-N1)    ∀E MINUS1 SUCCN , N1 

15  (¬((M*N1)=0)∧Q(SUCCN-N1,M*N1))⊃Q(PRED(SUCCN-N1),(M*N1)+M)  (6 13)  TAUT 

16  ∀N1.((SUCCN≥N1⊃Q(SUCCN-N1,M*N1))⊃(SUCCN≥SUCCN1⊃Q(SUCCN-SUCCN1,M*SUCCN1)))⊃∀N1.(SUCCN≥N1⊃Q(SUCCN-N1,M*N1))  (%
8)  TAUT 

17  ∀N.((¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(K=0)∧Q(I,K))⊃Q(PREDI,K+M))))⊃(¬Q(SUCCN,0)∨(Q(0,M*SUCCN)∨¬∀I K.((¬(K=0)∧Q(I,%
K))⊃Q(PREDI,K+M)))))⊃∀N.(¬Q(N,0)∨(Q(0,M*N)∨¬∀I K.((¬(K=0)∧Q(I,K))⊃Q(PREDI,K+M))))    TAUT